f2f+-pred{i:l}
f2f+-pred(es; ff; f2f+; sndr; rcvr; e'; e)
== (snd-it(ff; f2f+Req(f2f+); e; sndr; rcvr)
==  (a:es-E(es)
==  (((a c e  rcv-it(ff; f2f+Ack(f2f+); a; sndr; rcvr))
==  ( (x:es-E(es). (es-causl(es; a; x)  x c e)  (rcv-it(ff; f2f+Ack(f2f+); x; sndr; rcvr)))
==  ( (e' = fifoSender(ff)(sndr,a)))))
==  (snd-it(ff; f2f+Ack(f2f+); e; rcvr; sndr)
==   (a:es-E(es)
==   (((a c e  rcv-it(ff; f2f+Req(f2f+); a; rcvr; sndr))
==   ( (x:es-E(es). 
==   ( (es-causl(es; a; x)  x c e)  (rcv-it(ff; f2f+Req(f2f+); x; rcvr; sndr)))
==   ( (e' = fifoSender(ff)(rcvr,a))))) 

latex

---

clarification:

f2f+-pred{i:l}
f2f+-pred(es; ff; f2f+; sndr; rcvr; e'; e)
== (snd-it(ff; f2f+Req(f2f+); e; sndr; rcvr)
==  (a:es-E(es)
==  (((es-causle(es;a;e)  rcv-it(ff; f2f+Ack(f2f+); a; sndr; rcvr))
==  ( (x:es-E(es). 
==  ( (es-causl(es; a; x)  es-causle(es;x;e))  (rcv-it(ff; f2f+Ack(f2f+); x; sndr; rcvr)))
==  ( (e' = fifoSender(ff)(sndr,a)  es-E(es)))))
==  (snd-it(ff; f2f+Ack(f2f+); e; rcvr; sndr)
==   (a:es-E(es)
==   (((es-causle(es;a;e)  rcv-it(ff; f2f+Req(f2f+); a; rcvr; sndr))
==   ( (x:es-E(es). 
==   ( (es-causl(es; a; x)  es-causle(es;x;e))  (rcv-it(ff; f2f+Req(f2f+); x; rcvr; sndr)))
==   ( (e' = fifoSender(ff)(rcvr,a)  es-E(es))))) 

latex

Definitions	fifoSender(ff), f(a), es-E(es), s = t, f2f+Req(f2f+), rcv-it(ff; p; e; i; j), A, e c e', es-causl(es; e; e'), P  Q, P  Q, x:A. B(x), x:A. B(x), f2f+Ack(f2f+), snd-it(ff; p; e; i; j), P  Q
FDL editor aliases	f2f+-pred